COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%elepha.l[f89,jmc]	A try a the reservation program in logic
C00008 00003
C00014 00004	\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
C00015 ENDMK
C⊗;
%elepha.l[f89,jmc]	A try a the reservation program in logic
\input memo.tex[let,jmc]
\title{This is the key part needed to make the paper distributable.}
\section{Elephant Programs as Sentences of Logic}

	This is the most tentative section of the present draft.
At present we have two approaches to writing Elephant programs
as sentences of logic.  The first approach is analogous to Algol 50.
It is based on updating a state of the program and a state of the
world.  Of course, the functions updating the state of the world will
be only partially known.  Therefore, unknown functions will occur, and
the knowledge we have about the world will be expressed by subjecting
these functions to axioms.  The second approach expresses the program
and tentatively what we know about the world in terms of events.
The events occur at times determined by axioms.  We describe the
events that we assert to occur and rely on circumscription to limit
the set of occurrences to those that follow from the axioms given.
We begin with the Algol 50 approach.

	As with Algol 50, we use a state vector $\xi(t)$ for
the state of the program during operation.  The program is
expessed by a formula for $\xi(t+1)$.  Since the program
interacts with the world, we also have a state vector $world(t)$
of the world external to the computer.  Because we can't have
complete knowledge of the world, we can't expect to
express $world(t+1)$ by a single formula, but proving perlocutionary
specifications will involve assumptions about the functions
that determine how $world(t)$ changes.

	We have
%
$$\xi(t+1) = update(input world(t),\xi,t)$$
%
and
%
$$world(t+1) = worldf(output \xi(t),world,t).$$
%
Notice that we have written $\xi$ and $world$ on the right sides
of the two equations rather than $\xi(t)$ and $world(t)$, which
might have been expected.  This allows us to let $\xi(t+1)$ and
$world(t+1)$ depend on the whole past rather than just the present.
(It would also allow equations expressing dependence on the future,
but since we won't write such equations, we don't have to try to
make sense of that possibility).

	For the reservation program we might have
%
% val doubts the need for q=
$$\eqalign{update(i,\xi,t) = &qif i q= qrequest qmake qcommitment admit(psgr,flt)
∧ ¬full qc1(flt,\xi(t))\cr
% qc1 is a contents function
\quad qthen &qadjoin(\xi(t),qcommitment admit1(psgr,flt,seatf(\xi(t))),\cr
&qoutput(assert grantrequest admit1(psgr,flt,seatf(\xi(t)))))\cr
% what to do if the flight is full
%
qelseif& i q= qquery qexists qcommitment admit(psgr,flt)\cr
	&qthen (qlet ((x (search commitment admit1(psgr,flt,?seat)))\cr
	(if& (null x) (qadjoin (\xi t) NO) \cr
% VAL suggests that it is better to put a universal quantifier on the outside
}.$$
% What about a general form of query and of assertion?
% what about some answers or all answers?
% what about two pass translation to logical sentence via lisp program
% with history data structure, e.g. like Algol 50

% illocutionary = behavioral
% perlocutionary = accomplishment
% VAL suggests \xi(t+1) = update(i(t),\xi,t)
% and i(t) = input world(t)
% in order to write specifications and proofs for behavior w/o mentioning world

% prove correctness of simplified program with just one statement
\vfill\eject



 $$\eqalign{(∀psgr flt t)&(input t = request make commitment admit(psgr flt)\cr
	&\quad\quad ∧ ¬ holds(t,full flt)\cr
&⊃ (∃ seat) (holds(t,available(seat,flt)) ∧\cr
&\quad arises(t, commitment admit(psgr,flt, seat))\cr
	&\quad ∧ outputs(t,promise admit(psgr,flt,seat)))).\cr}$$

Note the use of $admit$ first with two argments and later with three.
We suppose that $admit$ actually has a large set of arguments with
default values.  When an $admit(\ldots )$ expression is encountered,
it is made obvious which arguments are being given values by the
expression and which get default values.  The signals for this are
the name of the variable or an actual named argment as in Common
Lisp.  The compiler will have to come up with a way of assigning
a seat from those available.

$$\eqalign{
(∀psgr flt t) &(input t = query exists commitment admit(psgr flt)\cr
&⊃ outputs(t,if exists(t, commitment admit(psgr flt)) then\cr
&confirm(commitment admit(psgr flt seat)) else deny(input t))\cr}$$

$$\eqalign{
(∀psgr flt t) &(input t = request cancel commitment admit(psgr,flt)\cr
&⊃ revoke(t,commitment admit(psgr,flt))\cr}$$

$$\eqalign{
(∀t x)(&exists(t,commitment x) ≡ (∃t')(t' < t ∧ arises(t, commitment x))\cr & ∧
(∀t'')(t' < t'' < t ⊃ ¬revoke(t, commitment x)))\cr}$$

$$\eqalign{
(∀psgr flt t) &(input t = request admit(psgr,flt)\cr & ⊃
if exists(t, commitment admit( psgr,flt)\cr &\quad\quad then outputs(t,
command(agent,admit(psgr,flt,seat))\cr &\quad \quad else outputs(t, command(agent,
don't admit (psgr,flt))))\cr}$$

	Asserting that certain outputs occur and that certain propositions
hold doesn't establish that others don't occur.   Therefore, the program
as given is to be supplemented by circumscribing certain predicates,
namely $arises$, $outputs$ and $revoke$.

Remarks:

	1. Proving that a program fulfills its commitments
seems to be just a matter of expressing a commitment as making
sure a certain sentence is true, e.g. that the passenger is
allowed on the airplane.  In that case, proving that the program
fulfills its commitments is just a matter of showing that the
sentences expressing the commitments follow from the sentence
expressing the program.  The problem now is to decide what
class of sentences to allow as expressing various kinds of
commitments.  If the commitments are to be externally
expressed as promises, then they have to belong to the
i-o language.

	2. Commitments are like specifications, but they are
to be considered as dynamic, i.e. specific commitments are
created as the program runs.  We can ask what are the
program's commitments when it is in a given state.  Indeed
we might even be able to ask the program what its commitments
are.

	3. An Elephant interpreter need only match the inputs
against the program statements with inputs as premisses.  It then
issues the outputs, performs the actions and asserts the other
conclusions of the statement.  The circumscriptions should not
have to be consulted, because they can be regarded as asserting
that the only events that occur are those specified in the
statements.  Here the situation is similar to that of logic
programming.  The circumscriptions {\it are} used in proving that
the program meets its specifications, e.g. fulfills its commitments.

	There is a theorem about this that remains to be
precisely formulated and then proved.  Making it provable
might involve some revisions of the formalism.

\noindent Vladimir's message

Maybe you don't need $holds$ at all. You can use these abbreviations instead:

$$available(t,seat,flt) ≡ ¬∃psgr exists(t,commitment admit(psgr,flt,seat)),$$
$$full(t,flt) ≡ ¬∃seat available(t,seat,flt).$$

\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
\smallskip\noindent{\fiverm This draft of elepha.l[f89,JMC]\ TEXed on \jmcdate\ at \theTime}
%File originated on 28-Nov-89
\vfill\eject\end